/* Bogor: An Extensible and Highly-Modular Model Checking Framework
 * Copyright (c) 2002-2005 Kansas State University
 *
 * This software is licensed using the SAnToS Laboratory Open Academic License.
 * You should have received a copy of the License in the top directory of this
 * software distribution package. If not, then write to
 * SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506, USA.
 *
 * The SAnToS Laboratory homepage is located at http://www.cis.ksu.edu/santos.
 * The Bogor homepage is located at http://bogor.projects.cis.ksu.edu.
 */
package edu.ksu.cis.projects.bogor.module;

import java.io.IOException;
import java.io.PrintWriter;
import java.text.DecimalFormat;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Properties;

import org.wxq.output.MyWriter;

import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.ast.Action;
import edu.ksu.cis.projects.bogor.ast.BlockTransformation;
import edu.ksu.cis.projects.bogor.ast.Exp;
import edu.ksu.cis.projects.bogor.ast.FSM;
import edu.ksu.cis.projects.bogor.ast.Global;
import edu.ksu.cis.projects.bogor.ast.InitialValue;
import edu.ksu.cis.projects.bogor.ast.InvokeTransformation;
import edu.ksu.cis.projects.bogor.ast.Local;
import edu.ksu.cis.projects.bogor.ast.Location;
import edu.ksu.cis.projects.bogor.ast.Transformation;
import edu.ksu.cis.projects.bogor.ast.Visibility;
import edu.ksu.cis.projects.bogor.ast.checker.ConstIntExpEvaluator;
import edu.ksu.cis.projects.bogor.module.backtrack.IActionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IEndStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IExceptionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.INextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IPostNextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.config.Domain;
import edu.ksu.cis.projects.bogor.module.config.ISelfDescribingModule;
import edu.ksu.cis.projects.bogor.module.config.OptionScope;
import edu.ksu.cis.projects.bogor.module.state.IState;
import edu.ksu.cis.projects.bogor.module.throwable.ArithmeticBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.AssertionBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BadMonitorBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BogorException;
import edu.ksu.cis.projects.bogor.module.throwable.CastBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExceptionThrownBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExtFailedBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IllFormedModelBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IndexOutOfBoundsBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.NullPointerBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.RangeBogorException;
import edu.ksu.cis.projects.bogor.module.value.IIntValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.module.value.IValueArray;
import edu.ksu.cis.projects.bogor.symboltable.FSMSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.type.BooleanType;
import edu.ksu.cis.projects.bogor.type.FunType;
import edu.ksu.cis.projects.bogor.type.Type;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Pair;
import edu.ksu.cis.projects.bogor.util.Triple;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.trove.custom.IntIntTable;
import edu.ksu.cis.projects.trove.custom.IntList;
import edu.ksu.cis.projects.trove.custom.IntObjectTable;

/**
 * @author <a href="mailto:robby@cis.ksu.edu">Robby </a>
 * @author <a href="mailto:matt@cis.ksu.edu">Matt Hoosier </a>
 * @version CVS $Revision: 1.86 $ $Date: 2005/08/15 20:27:48 $
 */
public class DefaultSearcher implements ISearcher, ISelfDescribingModule {
	// ~ Static variables/initializers
	// ..........................................

	protected static final String PRINT_VERBOSE_TRACE_ID = "printVerboseTrace";

	protected static final String PRINT_STATUS_ID = "printStatus";

	protected static final String TRAIL_EXT = "bogor-trails";

	protected static final String PRINT_COUNTER_EXAMPLES_ID = "printCounterExamples";

	protected static final String WRITE_TRAIL_FILE_ID = "writeTrailFile";

	protected static final String ALL_AS_ERRORS_ID = "allAsErrors";

	protected static final String MAX_ERRORS_ID = "maxErrors";

	protected static final String MAX_DEPTH_ID = "maxDepth";

	protected static final String MAX_INVISIBLE_MOVES_ID = "maxInvisibleMoves";

	protected static final String UPDATE_STATE_INCREMENT_ID = "updateStateIncrement";

	protected static final String UPDATE_TRANSITION_INCREMENT_ID = "updateTransitionIncrement";

	protected static final String INVARIANTS_ID = "invariants";

	protected static final String CHECK_BACKTRACK_ID = "checkBacktrack";

	// ~ Instance variables
	// .....................................................

	protected boolean printCounterExamples = false;

	protected boolean writeTrailFile = true;

	protected boolean allAsErrors = false;

	protected boolean printVerboseTrace = true;

	protected boolean printStatus = true;

	// note: currently does not support extension
	protected int maxErrors = 0;

	protected int maxDepth = Integer.MAX_VALUE >> 1;

	protected int updateStateIncrement = 10000;

	protected int maxInvisibleMoves = Integer.MAX_VALUE >> 1;

	protected long updateTransitionIncrement = 10000;

	protected boolean checkBacktrack = false;

	protected String[] invariants;

	protected PrintWriter pw;

	/**
	 * @uml.property name="backtrackingInfos"
	 */
	protected ArrayList<ITransformationBacktrackingInfo> backtrackingInfos;

	protected IBogorConfiguration bc;

	protected IActionTaker at;

	protected IBacktrackingInfoFactory bif;

	protected ICounterExampleWriter cew;

	protected IExpEvaluator ee;

	protected ISchedulingStrategist ss;

	/**
	 * @uml.property name="state"
	 */
	protected IState state;

	protected IStateFactory sf;

	protected IStateManager sm;

	protected ISearcher sr;

	protected ITransformer tr;

	protected IValueFactory vf;

	protected IProgressManager pm;

	protected SymbolTable symbolTable;

	protected boolean isInvisible;

	protected boolean seenState;

	protected int lastMovedThreadId;

	protected int stateId;

	protected int invisibleMoves;

	protected int currentDepth;

	protected int currentMaxDepth;

	protected int errors;

	protected int seenStates;

	protected long startTime;

	protected long transitions;

	protected long lastUpdatedTransitions;

	protected int lastUpdatedStates;

	// TODO WXQ
	private MyWriter myWriter1;
	private MyWriter myWriter2;
	private MyWriter myWriter3;
	private List<Integer> statesList;
	private List<Pair<String, Integer>> edges;

	// private int statesCounter = 0;

	// ~ Constructors
	// ...........................................................

	public DefaultSearcher() {
		statesList = new ArrayList<Integer>();
		edges = new ArrayList<Pair<String, Integer>>();

		myWriter1 = new MyWriter("D:/testcases/lts.dot");

		myWriter2 = new MyWriter("D:/testcases/transitions.txt");
		try {
			myWriter1.write("digraph G {\r\n");
		} catch (IOException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}

		myWriter3 = new MyWriter("D:/testcases/lts.graphxml");
		try {
			String head = "<graphml "
					+ "xmlns=\"http://graphml.graphdrawing.org/xmlns\" "
					+ "xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\" "
					+ "xsi:schemaLocation=\"http://graphml.graphdrawing.org/xmlns "
					+ "http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd\">"
					+ "\r\n";
			String label = "<key id=\"elabel\" for=\"edge\" attr.name=\"label\" attr.type=\"string\"/>"
					+ "\r\n";
			String graph = "<graph id=\"G\" edgedefault=\"directed\">" + "\r\n";

			myWriter3.write(head);
			myWriter3.write(label);
			myWriter3.write(graph);

		} catch (IOException e) {

		}

	}

	// ~ Methods
	// ................................................................

	/**
	 * @uml.property name="backtrackingInfos"
	 */
	public ArrayList<ITransformationBacktrackingInfo> getBacktrackingInfos() {
		return backtrackingInfos;
	}

	public String getCopyrightNotice() {
		return null;
	}

	public int getErrorCount() {
		return errors;
	}

	public IMessageStore setOptions(String key, Properties configuration) {
		assert ((key != null) && (configuration != null));

		final String PRINT_COUNTER_EXAMPLES_ID = key + "."
				+ DefaultSearcher.PRINT_COUNTER_EXAMPLES_ID;
		final String ALL_AS_ERRORS_ID = key + "."
				+ DefaultSearcher.ALL_AS_ERRORS_ID;
		final String MAX_ERRORS_ID = key + "." + DefaultSearcher.MAX_ERRORS_ID;
		final String MAX_DEPTH_ID = key + "." + DefaultSearcher.MAX_DEPTH_ID;
		final String MAX_INVISIBLE_MOVES_ID = key + "."
				+ DefaultSearcher.MAX_INVISIBLE_MOVES_ID;
		final String UPDATE_STATE_INCREMENT_ID = key + "."
				+ DefaultSearcher.UPDATE_STATE_INCREMENT_ID;
		final String UPDATE_TRANSITION_INCREMENT_ID = key + "."
				+ DefaultSearcher.UPDATE_TRANSITION_INCREMENT_ID;
		final String INVARIANTS_ID = key + "." + DefaultSearcher.INVARIANTS_ID;
		final String WRITE_TRAIL_FILE_ID = key + "."
				+ DefaultSearcher.WRITE_TRAIL_FILE_ID;
		final String PRINT_VERBOSE_TRACE_ID = key + "."
				+ DefaultSearcher.PRINT_VERBOSE_TRACE_ID;
		final String PRINT_STATUS_ID = key + "."
				+ DefaultSearcher.PRINT_STATUS_ID;

		final String CHECK_BACKTRACK_ID = key + "."
				+ DefaultSearcher.CHECK_BACKTRACK_ID;

		ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
		ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

		for (Iterator<Object> i = configuration.keySet().iterator(); i
				.hasNext();) {
			String optionId = (String) i.next();
			String value = configuration.getProperty(optionId);

			if (PRINT_VERBOSE_TRACE_ID.equals(optionId)) {
				try {
					printVerboseTrace = Boolean.valueOf(value).booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (WRITE_TRAIL_FILE_ID.equals(optionId)) {
				try {
					writeTrailFile = Boolean.valueOf(value).booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (PRINT_STATUS_ID.equals(optionId)) {
				try {
					printStatus = Boolean.valueOf(value).booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (PRINT_COUNTER_EXAMPLES_ID.equals(optionId)) {
				try {
					printCounterExamples = Boolean.valueOf(value)
							.booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (ALL_AS_ERRORS_ID.equals(optionId)) {
				try {
					allAsErrors = Boolean.valueOf(value).booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (CHECK_BACKTRACK_ID.equals(optionId)) {
				try {
					checkBacktrack = Boolean.valueOf(value).booleanValue();
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "boolean", value }));
				}
			} else if (MAX_ERRORS_ID.equals(optionId)) {
				try {
					maxErrors = Integer.parseInt(value);
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "int", value }));
				}
			} else if (MAX_DEPTH_ID.equals(optionId)) {
				try {
					maxDepth = Integer.parseInt(value);
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "int", value }));
				}
			} else if (MAX_INVISIBLE_MOVES_ID.equals(optionId)) {
				try {
					maxInvisibleMoves = Integer.parseInt(value);
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "int", value }));
				}
			} else if (UPDATE_STATE_INCREMENT_ID.equals(optionId)) {
				try {
					updateStateIncrement = Integer.parseInt(value);
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "int", value }));
				}
			} else if (UPDATE_TRANSITION_INCREMENT_ID.equals(optionId)) {
				try {
					updateTransitionIncrement = Integer.parseInt(value);
				} catch (Exception e) {
					errors.add(FileMessage.buildMessage(optionId,
							ConfigurationMessages.BAD_FORMAT, new String[] {
									optionId, "int", value }));
				}
			} else if (INVARIANTS_ID.equals(optionId)) {
				try {
					List<String> funIds = Util.splitCommaSeparatedList(value);
					invariants = funIds.toArray(new String[funIds.size()]);
				} catch (Exception e) {
					errors.add(FileMessage
							.buildMessage(
									optionId,
									ConfigurationMessages.BAD_FORMAT,
									new String[] {
											optionId,
											"comma-separated string list (no whitespace)",
											"\"" + value + "\"" }));
				}
			} else if (optionId.startsWith(key) && !optionId.equals(key)) {
				warnings.add(FileMessage.buildMessage(optionId,
						ConfigurationMessages.UNKNOWN_OPTION,
						new String[] { optionId }));
			}
		}

		return new DefaultMessageStore(errors, warnings);
	}

	/**
	 * @uml.property name="state"
	 */
	public IState getState() {
		return state;
	}

	/**
	 * Once we have decided to terminate exploration of a depth-first path (the
	 * precondition to this method), roll back changes until the first ancestor
	 * state with unexplored siblings is found. If such an ancestor is found,
	 * then execute one step on it and return <tt>true</tt>. If no explored
	 * ancestor branches are found, then backtracking unwinds the entire trace
	 * and the initial state is reached. A <tt>false</tt> return value signals
	 * this result.
	 */
	public boolean backtrack() {
		IState state = sr.getState();
		ArrayList<ITransformationBacktrackingInfo> stack = sr
				.getBacktrackingInfos();

		vf.backward();
		sf.backward();

		try {
			for (ListIterator<ITransformationBacktrackingInfo> tbiIter = stack
					.listIterator(stack.size()); tbiIter.hasPrevious();) {
				// Peek at the transformation
				ITransformationBacktrackingInfo tbi = tbiIter.previous();

				int threadId = tbi.getTransition().first;
				Transformation transformation = tbi.getTransition().second;

				vf.setContext(state, threadId);
				sf.setContext(state, threadId);

				currentDepth--;
				sf.getNotifier().notifyCurrentDepthChanged(currentDepth + 1,
						currentDepth);

				ArrayList<IPostNextStateBacktrackingInfo> postNextStateInfos = tbi
						.getPostNextStateBacktrackingInfos();
				ArrayList<INextStateBacktrackingInfo> nextStateInfos = tbi
						.getNextStateBacktrackingInfos();
				ArrayList<? extends IActionBacktrackingInfo> mainInfos = tbi
						.getMainTransformationBacktrackingInfos();

				// Roll back search metadata actions (property automaton
				// transitions,  coalescing data, etc)
				for (ListIterator<IPostNextStateBacktrackingInfo> pnsIter = postNextStateInfos
						.listIterator(postNextStateInfos.size()); pnsIter
						.hasPrevious();) {
					IPostNextStateBacktrackingInfo bi = pnsIter.previous();
					pnsIter.remove();

					bi.backtrack(state);

					// If nondeterminism still needs to be explored, then quit
					// rolling change back, restart from here, and exit
					if (!bi.getSchedulingStrategyInfo().isCovered()) {
						isInvisible = false;
						stateId = tbi.getStateId();
						seenState = false;

						vf.forward();
						sf.forward();

						doPostNextStateBookkeeping(tbi, bi);

						currentDepth++;
						sf.getNotifier().notifyCurrentDepthChanged(
								currentDepth - 1, currentDepth);

						if (sr.shouldStore()) {
							IStoreStateResult newState = sm.storeState(state);
							stateId = newState.getStateId();
							seenState = newState.isSeen();
						}

						return true;
					}
				}

				// Roll back actions to set up next-state
				for (ListIterator<INextStateBacktrackingInfo> nsIter = nextStateInfos
						.listIterator(nextStateInfos.size()); nsIter
						.hasPrevious();) {
					nsIter.previous().backtrack(state);
					nsIter.remove();
				}

				// Roll back main transformation body actions
				for (ListIterator<? extends IActionBacktrackingInfo> mainIter = mainInfos
						.listIterator(mainInfos.size()); mainIter.hasPrevious();) {
					IActionBacktrackingInfo bi = mainIter.previous();
					mainIter.remove();

					bi.backtrack(state);

					if (!bi.getSchedulingStrategyInfo().isCovered()) {
						isInvisible = false;
						stateId = tbi.getStateId();
						seenState = false;

						vf.forward();
						sf.forward();

						this.invisibleMoves = tbi.getInvisibleMoves();

						vf.setContext(state, threadId);
						sf.setContext(state, threadId);

						sr.doTransition(threadId, transformation,
								tbi.getAppropriateRestartPoint(bi), tbi);

						return true;

					}
				}

				//
				// All sub-parts of the transition have been rolled back
				// by now. Only nondeterminism on the selection of the overall
				// transition remains.
				//

				this.seenState = false;
				this.invisibleMoves = tbi.getInvisibleMoves();
				this.stateId = tbi.getStateId();
				this.lastMovedThreadId = tbi.getLastMovedThreadId();

				// Pop the transformation
				tbiIter.remove();
				tbi.backtrack(state);

				if (checkBacktrack) {
					assert sm.storeState(state).getStateId() == tbi
							.getStateId();
				}

				if (!tbi.getSchedulingStrategyInfo().isCovered()) {
					ArrayList<Pair<Integer, Transformation>> workSet = tbi
							.getWorkSet();
					ArrayList<Pair<Integer, Transformation>> enabledSet = tbi
							.getEnabledSet();

					ISchedulingStrategyInfo ssi = tbi
							.getSchedulingStrategyInfo();

					int workSetIndex = ss.advise(
							createContext(stateId, invisibleMoves, 0, state),
							workSet, ssi);

					Pair<Integer, Transformation> restartTransformation = workSet
							.get(workSetIndex);

					int[] tids = state.getThreadIds();
					Arrays.sort(tids);

					int canonicalThreadIndex = Util.search(tids,
							restartTransformation.first);

					ITransformationBacktrackingInfo newTbi;

					if (restartTransformation.second instanceof BlockTransformation) {
						newTbi = bif.createBlockTransformationBacktrackingInfo(
								stateId, invisibleMoves, isInvisible,
								lastMovedThreadId, enabledSet, workSet,
								workSet.get(workSetIndex),
								canonicalThreadIndex, ssi);
					} else {
						assert restartTransformation.second instanceof InvokeTransformation;

						newTbi = bif
								.createInvokeTransformationBacktrackingInfo(
										stateId, invisibleMoves, isInvisible,
										lastMovedThreadId, enabledSet, workSet,
										workSet.get(workSetIndex),
										canonicalThreadIndex, ssi);
					}

					sr.getBacktrackingInfos().add(newTbi);

					lastMovedThreadId = restartTransformation.first;

					vf.forward();
					sf.forward();
					vf.setContext(state, restartTransformation.first);
					sf.setContext(state, restartTransformation.first);

					sr.doTransition(restartTransformation.first,
							restartTransformation.second, null, newTbi);
					vf.removeContext();
					sf.removeContext();

					return true;
				}
			}

			// Okay... no transitions needing more exploration were found.
			// A null return value signifies the no restart is necessary.
			return false;
		} finally {
			vf.removeContext();
			sf.removeContext();

			vf.forward();
			sf.forward();
		}
	}

	public IMessageStore connect(IBogorConfiguration bc) {
		assert (bc != null);

		ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
		ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

		this.bc = bc;
		this.sr = bc.getSearcher();
		this.symbolTable = bc.getSymbolTable();
		this.at = bc.getActionTaker();
		this.cew = bc.getCounterExampleWriter();
		this.sm = bc.getStateManager();
		this.ss = bc.getSchedulingStrategist();
		this.tr = bc.getTransformer();
		this.ee = bc.getExpEvaluator();
		this.sf = bc.getStateFactory();
		this.vf = bc.getValueFactory();
		this.bif = bc.getBacktrackingInfoFactory();
		this.pm = bc.getProgressManager();
		this.pw = bc.getPrintWriter();

		// TODO: needs to check for invariants type
		if (invariants != null) {
			ArrayList<String> list = new ArrayList<String>();
			int size = invariants.length;
			Map<String, Type> funMap = symbolTable.getGlobalFunTable();

			for (int i = 0; i < size; i++) {
				String funId = invariants[i];
				Type type = funMap.get(funId);

				if (!(type instanceof FunType)) {
					errors.add(FileMessage.buildMessage(
							"No such invariant fun {0}.",
							new String[] { funId }));

					continue;
				}

				FunType fType = (FunType) type;

				if ((fType.getParamTypeCount() != 0)
						|| !(fType.getReturnType() instanceof BooleanType)) {
					errors.add(FileMessage.buildMessage(
							"Ill-formed invariant {0} of type {1}",
							new String[] { funId, fType.toString() }));

					continue;
				}

				list.add(funId);
			}

			size = list.size();

			if (size == 0) {
				invariants = null;
			} else {
				invariants = new String[size];

				for (int i = 0; i < size; i++) {
					invariants[i] = (String) list.get(i);
				}
			}
		}

		return new DefaultMessageStore(errors, warnings);
	}

	public IState createInitialState() {
		IStateFactoryArguments args = getInitialStateFactoryArguments();
		IState vanillaState = sf.createState(args);
		fillInitialVariableValues(vanillaState, args);
		return vanillaState;
	}

	public void dispose() {
		bc = null;
		symbolTable = null;
		at = null;
		sm = null;
		ss = null;
		tr = null;
		ee = null;
		sf = null;
		vf = null;
		bif = null;
		pm = null;
		pw = null;
		sr = null;

		if (cew != null) {
			cew.dispose();
			cew = null;
		}
	}

	public void doTransition(int threadId, Transformation t, Action a,
			ITransformationBacktrackingInfo container) {
		assert (t != null);
//		int preID = this.stateId;
		ISchedulingStrategyContext ssc = createContext(stateId, invisibleMoves,
				threadId, state);

		isInvisible = t.getVisibility() == Visibility.INVISIBLE;

		doTransition(ssc, t, a, isInvisible, container);
		doPostNextStateBookkeeping(container, null);

		IExceptionBacktrackingInfo raisedException = Util.findLast(
				container.getNextStateBacktrackingInfos(),
				IExceptionBacktrackingInfo.class);

		if ((raisedException != null && raisedException.isUncaught())
				|| !state.isThreadAlive(threadId)
				|| invisibleMoves >= maxInvisibleMoves) {
			isInvisible = false;
		}

		sr.store();

		// TODO WXQ
		if (sr.shouldStore()) {

			// TODO wxq
			/*if (!states.contains(stateId)) {
				// this.statesCounter++;
				states.add(stateId);
				try {
					myWriter3.write("<node id=\"" + stateId + "\"/>\r\n");
				} catch (Exception e) {
					e.printStackTrace();
				}
			}
*/
			String transID = container.getTransition().first + "-"
					+ container.getTransition().second.hashCode();
			int preID = container.getStateId();
			try {
//				 if(stateId>2200){

				if (!edges.contains(new Pair(transID,preID)) ){
					if(!statesList.contains(preID)){
						statesList.add(preID);
						myWriter3.write("<node id=\"" + preID + "\"/>\r\n");
					}
					if(!statesList.contains(stateId)){
						statesList.add(stateId);
						myWriter3.write("<node id=\"" + stateId + "\"/>\r\n");
					}
					edges.add(new Pair(transID, preID));
					// Lts file
					
//					if((stateId-preID)!=1){
						Transformation tran = container.getTransition().second;
						FSM fsm = tran.getParent().getParent();
						String name = fsm.getDeclarationKeyword().getName();
						if (name.equals("function")){
							
							
						}
						
						
						
						
					myWriter1.write(preID + "->" + stateId);
					myWriter1.write(" [label=\"" + transID + "\"]");
					myWriter1.write(";\r\n");
					myWriter1.flush();
//					}
					

					// transitions list
					myWriter2.write(transID + "\t" + container.getTransition());
					myWriter2.write(container.getTransition().second.getLocationInfo().getLine1()+"--");
					myWriter2.write(container.getTransition().second.getParent().getParent().getId());
					myWriter2.write(";\r\n");
					
					myWriter2.flush(); 

					myWriter3.write("<edge id=\"" + edges.size() + "\""
							+ " source=\"" + container.getStateId() + "\""
							+ " target=\"" + stateId + "\">" + "\r\n"
							+ "<data key=\"elabel\">" + transID + "</data>"
							+ "\r\n" + "</edge>" + "\r\n");
					myWriter3.flush();
				}

				// }
			} catch (Exception e) {

			}
		}

		transitions++;
		currentDepth++;
		sf.getNotifier().notifyCurrentDepthChanged(currentDepth - 1,
				currentDepth);

		if (currentDepth > currentMaxDepth) {
			currentMaxDepth = currentDepth;
		}

		// System.out.println(preID + "-->" +stateId);

		if (printStatus) {
			int numStates = sm.getStateCount();
			int totalStates = numStates + seenStates;

			if ((lastUpdatedStates <= totalStates)
					|| (lastUpdatedTransitions <= transitions)) {
				lastUpdatedStates += updateStateIncrement;
				lastUpdatedTransitions += updateTransitionIncrement;
				pm.update(transitions, numStates, seenStates, currentDepth,
						currentMaxDepth, errors, System.currentTimeMillis()
								- startTime, false);
			}
		}
	}

	public void error(int errCode) {
		// be sure that error state is always in state manager
		sm.storeState(state);

		errors++;

		pw.println();

		if (printCounterExamples) {
			pw.println("*** Begin Error Trace ***");

			for (Iterator<ITransformationBacktrackingInfo> iter = sr
					.getBacktrackingInfos().iterator(); iter.hasNext();) {
				ITransformationBacktrackingInfo transition = iter.next();

				int thread = transition.getTransition().first;
				Transformation transformation = transition.getTransition().second;

				pw.printf("Thread#%d, Line#%d, FSM:%s, Loc:%s", thread,
						transformation.getLocationInfo().getLine1(),
						transformation.getParent().getParent().getId(),
						transformation.getParent().getId());

				pw.println();
				pw.println(transformation);
				pw.println();
			}

			pw.println("*** End Error Trace ***");
		}

		pw.print("[Time: ");
		pw.print(System.currentTimeMillis() - startTime);
		pw.print(" ms, Depth: ");
		pw.print(currentDepth);
		pw.print("] Error found: ");

		String reason = null;

		// Do this once, rather than duplicating the code
		// for each upcoming "case" branch...
		pm.update(transitions, sm.getStateCount(), seenStates, currentDepth,
				currentMaxDepth, errors,
				System.currentTimeMillis() - startTime, false);

		switch (errCode) {
		case ILL_FORMED_MODEL_CODE:
			pm.signalIllFormedModel();
			pw.println(reason = "Ill-formed model");

			break;

		case INVALID_END_STATE_CODE:
			pm.signalInvalidEndState();
			pw.println(reason = "Invalid end state");

			break;

		case ASSERTION_FAILED_CODE:
			pm.signalAssertionFailure();
			pw.println(reason = "Assertion failed");

			break;

		case RANGE_EXCEPTION_CODE:
			pm.signalRangeException();
			pw.println(reason = "Range exception");

			break;

		case UNCAUGHT_EXCEPTION_CODE:
			pm.signalUncaughtException();
			pw.print(reason = "Uncaught exception: ");

			ITransformationBacktrackingInfo tbi = sr.getBacktrackingInfos()
					.get(sr.getBacktrackingInfos().size() - 1);
			IExceptionBacktrackingInfo xbi = Util.findLast(
					tbi.getNextStateBacktrackingInfos(),
					IExceptionBacktrackingInfo.class);

			if (xbi != null) {
				assert xbi.isUncaught();
				BogorException be = xbi.getThrownException();

				if (be instanceof ArithmeticBogorException) {
					pw.println("arithmetic (e.g., divide by zero)");
				} else if (be instanceof BadMonitorBogorException) {
					pw.println("cad monitor");
				} else if (be instanceof CastBogorException) {
					pw.println("cast");
				} else if (be instanceof IndexOutOfBoundsBogorException) {
					pw.println("index out of bounds");
				} else if (be instanceof NullPointerBogorException) {
					pw.println("null pointer");
				} else if (be instanceof ExceptionThrownBogorException) {
					ExceptionThrownBogorException etbe = (ExceptionThrownBogorException) be;
					pw.println(etbe.getThrowableName());
				}
			}
			break;

		case EXT_FAILED_CODE:
			pm.signalExtFailure();
			pw.println(reason = "Ext failed");

			break;

		case INVARIANT_VIOLATED_CODE:
			pm.signalInvariantViolation();
			pw.println(reason = "Invariant violated");

			break;

		default:
			assert false;

			break;
		}

		if (!allAsErrors) {
			storeCounterExample(sr.getBacktrackingInfos(), stateId,
					invisibleMoves, reason);
		}

		pw.println();

		if (errors == maxErrors) {
			throw new MaxErrorReachedException();
		}
	}

	public void initialize() {
		backtrackingInfos = new ArrayList<ITransformationBacktrackingInfo>();
		isInvisible = false;
		lastMovedThreadId = -1;
		invisibleMoves = 0;
		transitions = 0;
		lastUpdatedStates = 0;
		lastUpdatedTransitions = 0;
		errors = 0;
		seenStates = 0;
		currentDepth = 0;

		state = sr.createInitialState();
		stateId = sm.storeState(state).getStateId();

		vf.forward();
		sf.forward();
	}

	public void search() {
		System.gc();

		pw.println("");

		String startMemoryMsg = "Total memory before search: "
				+ getMemory(Runtime.getRuntime().totalMemory()
						- Runtime.getRuntime().freeMemory());

		boolean maxDepthReached = false;

		startTime = System.currentTimeMillis();
		/*try {
			myWriter3.write("<node id=\"" + stateId + "\"/>\r\n");
		} catch (Exception e) {
			e.printStackTrace();
		}*/

		try {
			while (!pm.shouldTerminate()) {
				if (currentDepth > maxDepth) {
					if (allAsErrors) {
						// TODO: change to call to error()
						errors++;
						storeCounterExample(sr.getBacktrackingInfos(), stateId,
								invisibleMoves, "Max Depth Reached");

						if (errors == maxErrors) {
							throw new MaxErrorReachedException();
						}
					}

					currentMaxDepth--;
					maxDepthReached = true;
					pm.signalMaxDepthReached();

					if (!sr.backtrack()) {
						// finish
						break;
					}
				} else {
					// int preStateId = stateId;
					boolean flag = !sr.step();
					if (flag) {
						if (allAsErrors) {
							// TODO: change to call to error()
							errors++;
							storeCounterExample(sr.getBacktrackingInfos(),
									stateId, invisibleMoves,
									"Seen Before or End State");

							if (errors == maxErrors) {
								throw new MaxErrorReachedException();
							}
						}

						if (!sr.backtrack()) {
							// finish
							break;
						}
					}
				}

				// handle uncaught BIR-level exceptions
//				checkExceptions();

				if (!checkInvariants()) {
					sr.error(INVARIANT_VIOLATED_CODE);

					if (!sr.backtrack()) {
						// finish
						break;
					}
				}
			}
		} catch (MaxErrorReachedException mce) {
		} catch (OutOfMemoryError oeme) {
			pm.signalOutOfMemory();
			pw.println("Out of memory!!!");
		} finally {
			try {
				this.myWriter1.write("}");
			} catch (IOException e) {
				// TODO Auto-generated catch block
				e.printStackTrace();
			}
			this.myWriter1.close();
			this.myWriter2.close();
			try {
				myWriter3.write("</graph>");
				myWriter3.write("</graphml>");

			} catch (IOException e) {
				e.printStackTrace();
			}
			this.myWriter3.close();
		}

		long endTime = System.currentTimeMillis();

		System.gc();

		pm.update(transitions, sm.getStateCount(), seenStates, currentDepth,
				currentMaxDepth, errors, endTime - startTime, true);

		if (maxDepthReached) {
			pw.println("");
			pw.println("Max depth reached!!!");
			pw.println("");
		}

		System.gc();

		int states = sm.getStateCount();
		long processingTime = endTime - startTime;

		System.gc();

		pw.println(startMemoryMsg);
		pw.println("Total memory after search: "
				+ getMemory(Runtime.getRuntime().totalMemory()
						- Runtime.getRuntime().freeMemory()));
		pw.println("Total search time: " + processingTime + " ms ("
				+ getTime(processingTime) + ")");
		pw.println("States count: " + states);
		pw.println("Matched states count: " + seenStates);
		pw.println("Max depth: " + currentMaxDepth);
		pw.flush();

		sr.writeCounterExamples();

		pw.println("Done!");
		pw.flush();

		return;
	}

	public boolean shouldStore() {
		return checkBacktrack || !isInvisible;
	}

	public boolean step() {
		if (shouldBacktrack() || seenState) {
			return false;
		}

		final int[] runnableThreadIds = state.getThreadIds();

		if (runnableThreadIds.length == 0) {
			return false;
		}

		IntObjectTable<ArrayList<Transformation>> workSet;
		IntObjectTable<ArrayList<Transformation>> enabledSet;

		try {
			if (isInvisible) {
				IEnabledTransformationsContext ctx = createContext(state,
						stateId, invisibleMoves,
						new int[] { lastMovedThreadId });

				enabledSet = ss.getEnabledTransformations(ctx);
				workSet = ss.getWorkSet(ctx, enabledSet);

				if (workSet.size() == 0) {
					isInvisible = false;

					if (!sr.store()) {
						return false;
					}

					ctx = createContext(state, stateId, invisibleMoves,
							runnableThreadIds);

					enabledSet = ss.getEnabledTransformations(ctx);
					workSet = ss.getWorkSet(ctx, enabledSet);
				}
			} else {
				IEnabledTransformationsContext ctx = createContext(state,
						stateId, invisibleMoves, runnableThreadIds);

				enabledSet = ss.getEnabledTransformations(ctx);
				workSet = ss.getWorkSet(ctx, enabledSet);
			}
		} catch (IllFormedModelBogorException ifmmce) {
			sr.error(ILL_FORMED_MODEL_CODE);

			pw.println(ifmmce.getNode());
			pw.println();

			return false;
		}

		int workSetSize = 0;

		for (int key : workSet.keys()) {
			workSetSize += workSet.get(key).size();
		}

		if (workSetSize == 0) {
			sr.error(INVALID_END_STATE_CODE);
			return false;
		}

		int enabledSetSize = 0;

		for (int key : enabledSet.keys()) {
			enabledSetSize += enabledSet.get(key).size();
		}

		ISchedulingStrategyInfo ssi = ss.newStrategyInfo();

		ArrayList<Pair<Integer, Transformation>> flattenedWorkSet = makeChoices(workSet);

		ArrayList<Pair<Integer, Transformation>> flattenedEnabledSet = makeChoices(enabledSet);

		// Ask scheduler which entry from workset to use
		Pair<Integer, Transformation> workSetEntry = flattenedWorkSet.get(ss
				.advise(createContext(stateId, invisibleMoves, 0, state),
						flattenedWorkSet, ssi));

		int[] tids = state.getThreadIds();
		Arrays.sort(tids);

		int canonicalThreadIndex = Util.search(tids, workSetEntry.first);

		ITransformationBacktrackingInfo container;

		if (workSetEntry.second instanceof BlockTransformation) {
			container = bif.createBlockTransformationBacktrackingInfo(stateId,
					invisibleMoves, isInvisible, lastMovedThreadId,
					flattenedEnabledSet, flattenedWorkSet, workSetEntry,
					canonicalThreadIndex, ssi);
		} else {
			container = bif.createInvokeTransformationBacktrackingInfo(stateId,
					invisibleMoves, isInvisible, lastMovedThreadId,
					flattenedEnabledSet, flattenedWorkSet, workSetEntry,
					canonicalThreadIndex, ssi);
		}

		sr.getBacktrackingInfos().add(container);

		/*
		 * if (workSetEntry.second.getVisibility() != Visibility.INVISIBLE) {
		 * System.out.println(workSetEntry.first + "\t" + workSetEntry.second);
		 * }
		 */

		lastMovedThreadId = workSetEntry.first;

		vf.setContext(state, workSetEntry.first);
		sf.setContext(state, workSetEntry.first);

		sr.doTransition(workSetEntry.first, workSetEntry.second, null,
				container);

		sf.removeContext();

		return true;
	}

	/**
	 * Rolls back the state to the moment just before the most recent
	 * transition.
	 * 
	 * @param state
	 *            system state to revert
	 * @param backtrackingInfos
	 *            stack of reverse deltas to roll back state
	 * @return the <code>ITransformationsBacktrackingInfo</code> of the most
	 *         recent transition (incomplete)
	 */

	public boolean stepBackward() {
		ArrayList<ITransformationBacktrackingInfo> stack = sr
				.getBacktrackingInfos();
		IState state = sr.getState();

		if (stack.isEmpty()) {
			return false;
		}

		// Pop last transition off stack
		ITransformationBacktrackingInfo tbi = stack.remove(stack.size() - 1);

		vf.backward();
		sf.backward();

		int threadId = tbi.getTransition().first;

		vf.setContext(state, threadId);
		sf.setContext(state, threadId);

		currentDepth--;
		sf.getNotifier().notifyCurrentDepthChanged(currentDepth + 1,
				currentDepth);

		ArrayList<IPostNextStateBacktrackingInfo> postNextStateInfos = tbi
				.getPostNextStateBacktrackingInfos();
		ArrayList<INextStateBacktrackingInfo> nextStateInfos = tbi
				.getNextStateBacktrackingInfos();
		ArrayList<? extends IActionBacktrackingInfo> mainInfos = tbi
				.getMainTransformationBacktrackingInfos();

		// Roll back search metadata actions (property automaton
		// transitions,
		// state coalescing data, etc)
		for (ListIterator<IPostNextStateBacktrackingInfo> pnsIter = postNextStateInfos
				.listIterator(postNextStateInfos.size()); pnsIter.hasPrevious();) {
			IPostNextStateBacktrackingInfo bi = pnsIter.previous();
			pnsIter.remove();

			bi.backtrack(state);
		}

		// Roll back actions to set up next-state
		for (ListIterator<INextStateBacktrackingInfo> nsIter = nextStateInfos
				.listIterator(nextStateInfos.size()); nsIter.hasPrevious();) {
			nsIter.previous().backtrack(state);
			nsIter.remove();
		}

		// Roll back main transformation body actions
		for (ListIterator<? extends IActionBacktrackingInfo> mainIter = mainInfos
				.listIterator(mainInfos.size()); mainIter.hasPrevious();) {
			IActionBacktrackingInfo bi = mainIter.previous();
			mainIter.remove();

			bi.backtrack(state);
		}

		//
		// All sub-parts of the transition have been rolled back
		// by now. Only nondeterminism on the selection of which
		// transition remains.
		//

		this.invisibleMoves = tbi.getInvisibleMoves();
		this.stateId = tbi.getStateId();
		this.lastMovedThreadId = tbi.getLastMovedThreadId();

		isInvisible = false;
		stateId = tbi.getStateId();
		seenState = false;

		tbi.backtrack(state);

		vf.removeContext();
		sf.removeContext();

		vf.forward();
		sf.forward();

		return true;
	}

	public boolean store() {
		if (sr.shouldStore()) {
			IStoreStateResult result = sm.storeState(state);
			stateId = result.getStateId();
			seenState = result.isSeen();
			invisibleMoves = 0;

			if (seenState) {
				seenStates++;

				return false;
			}
		} else {
			invisibleMoves++;
		}

		return true;
	}

	public void writeCounterExamples() {
		if (writeTrailFile) {
			cew.writeCounterExamples();
		}
	}

	protected FSMSymbolTable getFSMSymbolTable(int locDesc) {
		return symbolTable.getFSMSymbolTable(locDesc);
	}

	protected FSMSymbolTable getFSMSymbolTable(IState state, int threadId) {
		int locDesc = state.getLocation(threadId);

		return getFSMSymbolTable(locDesc);
	}

	protected IStateFactoryArguments getInitialStateFactoryArguments() {
		// construct reverse (index --> name) globals identifier mapping
		IntObjectTable<String> globalNameMap = new IntObjectTable<String>();

		{
			for (String key : symbolTable.getGlobalIndexTable().keySet(true)) {
				globalNameMap.put(symbolTable.getGlobalIndexTable().get(key),
						key);
			}
		}

		ArrayList<Type> globalTypes = symbolTable.getGlobalTypes();
		int globalsCount = globalTypes.size();
		IValue[] globalValues = new IValue[globalsCount];

		for (int i = 0; i < globalsCount; i++) {
			String name = globalNameMap.get(i);
			Global astNode = (Global) symbolTable.getIdentifierDefTable().get(
					name);
			Type globalType = globalTypes.get(i);

			// For now, we just create the default value. A global
			// whose initial value was specified in the model will
			// be initialized immediately after the IState is instantiated.
			globalValues[i] = vf.createDefaultValue(globalType);
		}

		final IValueArray globalValueArray = vf
				.newVariedValueArray(globalValues);

		final IntObjectTable<IValueArray> threadLocalValuesTable = new IntObjectTable<IValueArray>();
		final IntIntTable threadLocationTable = new IntIntTable();

		// loop over each thread type defined to instantiate any active ones
		for (FSMSymbolTable fsmSymbolTable : symbolTable.getFunctionTable()
				.values()) {
			FSM fsm = fsmSymbolTable.getFSM();

			// if the isn't an active type, then no default instance is
			// created
			if (!shouldActivateThread(fsm)) {
				continue;
			}

			int numCopies = fsm.getOptionalActiveMultiplicityExp() != null ? new ConstIntExpEvaluator(
					symbolTable).getValue(
					fsm.getOptionalActiveMultiplicityExp()).intValue() : 1;

			for (int j = 0; j < numCopies; j++) {
				ArrayList<Type> localTypes = fsmSymbolTable.getLocalTypes();
				int localsCount = localTypes.size();
				int argsCount = fsm.getParamCount();

				// All active thread types have exactly zero or one
				// parameters.
				assert (argsCount == 0) || (argsCount == 1);

				IValue[] localValues = new IValue[localsCount + argsCount];

				for (int k = 0; k < argsCount; k++) {
					// The single allowed parameter to an active thread
					// type is an integer giving its index in the
					// replicated thread array.
					// Type-checker should enforce that type of
					// this parameter is integer.
					localValues[k] = vf.newIntValue(j);
				}

				for (int k = 0; k < localsCount; k++) {
					Local astLocal = fsm.getLocal(k);
					Type localType = localTypes.get(k);

					// Just give the local the default values for now. If an
					// initial value was specified, it will be filled in
					// immediately after the IState is instantiated.
					localValues[k + argsCount] = vf
							.createDefaultValue(localType);
				}

				IValueArray localValueArray = vf
						.newVariedValueArray(localValues);

				int tid = sf.newThreadDescriptor();

				String locId = fsmSymbolTable.getInitialLocation();
				final int locDesc = fsmSymbolTable.getLocationDescTable().get(
						locId);

				threadLocalValuesTable.put(tid, localValueArray);
				threadLocationTable.put(tid, locDesc);
			}
		}

		return new IStateFactoryArguments() {
			public IValueArray getGlobalValues() {
				return globalValueArray;
			}

			public IValueArray getLocalValues(int threadId) {
				assert threadLocalValuesTable.containsKey(threadId);

				return threadLocalValuesTable.get(threadId);
			}

			public int getLocationDesc(int threadId) {
				assert threadLocalValuesTable.containsKey(threadId);

				return threadLocationTable.get(threadId);
			}

			public int[] getThreadIds() {
				return threadLocationTable.keys();
			}
		};
	}

	protected Location getLocation(IState state, int threadId) {
		int locDesc = state.getLocation(threadId);

		return getLocation(locDesc);
	}

	protected Location getLocation(int locDesc) {
		String locId = symbolTable.getLocDescLocIdTable()[locDesc];
		Location l = getFSMSymbolTable(locDesc).getLocationDefTable()
				.get(locId);

		return l;
	}

	protected String getMemory(long mem) {
		return new DecimalFormat("#,###").format(mem) + " bytes ("
				+ new DecimalFormat("#,###.##").format(mem / 1024.0 / 1024.0)
				+ " Mb)";
	}

	protected String getTime(long time) {
		int hours = (int) (time / 3600000);
		time = time - (hours * 3600000L);

		int minutes = (int) (time / 60000);
		time = time - (minutes * 60000L);

		int seconds = (int) (time / 1000);

		return hours + ":" + minutes + ":" + seconds;
	}

	protected void addAll(ArrayList<IBacktrackingInfo> result,
			IBacktrackingInfo[] bis) {
		int size = bis.length;

		for (int i = 0; i < size; i++) {
			result.add(bis[i]);
		}
	}

	protected void checkExceptions() {
		ArrayList<ITransformationBacktrackingInfo> stack = sr
				.getBacktrackingInfos();

		if (!stack.isEmpty()) {
			ITransformationBacktrackingInfo lastTbi = stack
					.get(stack.size() - 1);

			IExceptionBacktrackingInfo xbi = Util.findLast(
					lastTbi.getNextStateBacktrackingInfos(),
					IExceptionBacktrackingInfo.class);

			if (xbi != null && xbi.isUncaught()) {
				BogorException mce = xbi.getThrownException();

				if (mce instanceof AssertionBogorException) {
					sr.error(ASSERTION_FAILED_CODE);
				} else if (mce instanceof RangeBogorException) {
					sr.error(RANGE_EXCEPTION_CODE);
				} else if (mce instanceof ExtFailedBogorException) {
					sr.error(EXT_FAILED_CODE);
				} else if (mce instanceof ExceptionThrownBogorException) {
					sr.error(UNCAUGHT_EXCEPTION_CODE);
				}
			}
		}
	}

	protected boolean checkInvariants() {
		if (invariants == null) {
			return true;
		}

		int size = invariants.length;
		boolean result = true;

		for (int i = 0; (i < size) && result; i++) {
			String funId = invariants[i];
			ISchedulingStrategyInfo ssi = ss.newStrategyInfo();
			ISchedulingStrategyContext ssc = createContext(-1, -1, -1, state);

			ee.setSchedulingStrategyContextInfo(ssc, ssi);

			do {
				IValue val = ee.evaluateApply(funId, new IValue[0]);
				assert val instanceof IIntValue;

				if (((IIntValue) val).getInteger() == 0) {
					result = false;
				}
			} while (!ssi.isCovered());

			ee.unsetSchedulingStrategyContextInfo();
		}

		return result;
	}

	protected ISchedulingStrategyContext createContext(final int stateId,
			final int invisibleMoves, final int threadId, final IState state) {
		return new ISchedulingStrategyContext() {
			public void dispose() {
			}

			public int getExtDesc() {
				return 0;
			}

			public IState getState() {
				return state;
			}

			public int getInvisibleMoves() {
				return invisibleMoves;
			}

			public int getThreadId() {
				return threadId;
			}

			public int getStateId() {
				return stateId;
			}
		};
	}

	protected IEnabledTransformationsContext createContext(final IState state,
			final int stateId, final int invisibleMoves, final int[] threadIds) {
		return new IEnabledTransformationsContext() {
			public IState getState() {
				return state;
			}

			public int getStateId() {
				return stateId;
			}

			public int getInvisibleMoves() {
				return invisibleMoves;
			}

			public int[] getThreadIds() {
				return threadIds;
			}
		};
	}

	/**
	 * <p>
	 * Perform any steps needed to update the machinery after the main
	 * transition has been executed. Property automaton moves, updates to
	 * fields, etc. <em>Every</em> action performed inside the scope of this
	 * method should be reversible via an <tt>IBacktrackingInfo</tt>. The
	 * reverse actions should be added to the end of <tt>container</tt>'s
	 * {@link ITransformationBacktrackingInfo#getPostNextStateBacktrackingInfos()
	 * post-next state undo actions} collection.
	 * </p>
	 * <p>
	 * Note that the parameter <tt>restartPoint</tt> may indicate a point from
	 * which the machinery updates should begin. This is used in the case that
	 * backtracking detects one of the actions inserted onto the stack from a
	 * prior invocation of <tt>doPostNextStateBookkeeping()</tt> needs further
	 * exploration. In this case, the exact backtracking record put on the stack
	 * last time is passed in as a reference item. Its scheduling information (
	 * <tt>restartPoint.getSchedulingStrategyInfo()</tt>) should be used to help
	 * determine the next branch to explore.
	 * </p>
	 * <p>
	 * In the case that <tt>restartPoint</tt> is specified (not <tt>null</tt>),
	 * an implementor is obliged to check whether its runtime type corresponds
	 * to any action which they (not the base class) have put onto the stack. If
	 * so, then no recursive call to <tt>super.doPostNextStateBookkeeping()</tt>
	 * is made. If <tt>restartPoint</tt> is not <tt>null</tt> but its runtime
	 * type does not match any item explicitly put onto the stack by the
	 * implementor, then the superclass's implementation should be invoked in
	 * order to allow <em>its</em> implementor the opportunity to handle the
	 * not-yet-fully-explored branch point. An example:
	 * </p>
	 * 
	 * <pre>
	 *  protected void doPostNextStateBookkeeping(
	 *      ITransformationBacktrackingInfo container,
	 *      IPostNextStateBacktrackingInfo restartPoint)
	 *  {
	 *      if (restartPoint instanceof IPrivateFieldUpdateBacktrackingInfo)
	 *      {
	 *          updatePrivateField(
	 *              container,
	 *              (IPrivateFieldUpdateBacktrackingInfo) restartPoint);
	 *      }
	 *      else
	 *      {
	 *          super.doPostNextStateBookkeeping(container, restartPoint);
	 *          updatePrivateField(container, null);
	 *      }
	 *  }
	 *  
	 *  protected void updatePrivateField(
	 *      IPostNextStateBacktrackingInfo container,
	 *      IPrivateFieldUpdateBacktrackingInfo restartPoint)
	 *  {
	 *      final ISchedulingStrategyInfo ssi = restartPoint == null
	 *          ? ss.newStrategyInfo()
	 *          : restartPoint.getSchedulingStrategyInfo();
	 *           
	 *      final int oldValue = this.someFunkyVariable;
	 *      
	 *      int newValue = ... ;
	 *      
	 *      this.someFunkyVariable = newValue;
	 *      
	 *      container.getPostNextStateBacktrackingInfos().add(
	 *          new IPrivateFieldUpdateBacktrackingInfo()
	 *              {
	 *                  ...
	 *                  
	 *                  public void backtrack(IState state)
	 *                  {
	 *                      someFunkyVariable = oldValue;
	 *                  }
	 *                  
	 *                  public ISchedulingStrategyInfo getSchedulingStrategyInfo()
	 *                  {
	 *                      return ssi;
	 *                  }
	 *                  
	 *                  ...
	 *              });
	 *  }
	 * </pre>
	 */
	protected void doPostNextStateBookkeeping(
			ITransformationBacktrackingInfo container,
			IPostNextStateBacktrackingInfo restartPoint) {
		// do nothing in default version
	}

	protected void doTransition(ISchedulingStrategyContext ssc,
			Transformation t, Action a, boolean isInvisible,
			ITransformationBacktrackingInfo container) {
		/*
		 * if(!isInvisible){ System.out.println(stateId + "-->" +
		 * t.getNextState()); }
		 */
		if (t instanceof BlockTransformation) {
			BlockTransformation bt = (BlockTransformation) t;
			tr.transform(ssc, bt, isInvisible, a, container);
		} else if (t instanceof InvokeTransformation) {
			InvokeTransformation it = (InvokeTransformation) t;
			tr.transform(ssc, it, isInvisible, false, null, container);
		} else {
			assert false;
		}
	}

	protected ArrayList<ICounterExampleSchedulingInfo> extractErrorSchedule(
			ArrayList<ITransformationBacktrackingInfo> stack) {
		ArrayList<ICounterExampleSchedulingInfo> result = new ArrayList<ICounterExampleSchedulingInfo>();

		for (Iterator<ITransformationBacktrackingInfo> transitions = stack
				.iterator(); transitions.hasNext();) {
			IntList currNumOfChoices = new IntList();
			IntList currChosenIndices = new IntList();

			ITransformationBacktrackingInfo tbi = transitions.next();
			Pair<Integer, Transformation> transition = tbi.getTransition();

			// find index of transition.second in containing Location
			int transformationIndex = 0;
			while (transition.second != transition.second.getParent()
					.getTransformation(transformationIndex)) {
				transformationIndex++;
			}

			// record how many children the location had, and which offset in
			// this set of children was actually taken
			currNumOfChoices.add(transition.second.getParent()
					.getTransformationCount());
			currChosenIndices.add(transformationIndex);

			// record all nondeterministic scheduling decisions made during
			// execution of main transition body
			for (Iterator<IActionBacktrackingInfo> actions = tbi
					.getMainTransformationBacktrackingInfos().iterator(); actions
					.hasNext();) {
				ISchedulingStrategyInfo ssi = actions.next()
						.getSchedulingStrategyInfo();

				for (int i = 0; i < ssi.getInfoCount(); i++) {
					currNumOfChoices.add(ssi.getChoiceCount(i));
					currChosenIndices.add(ssi.getChosenIndex(i));
				}
			}

			// next-state backtracking actions are defined not to be
			// nondeterministic, so we don't bother looking in them

			// record all nondeterministic scheduling decisions made to
			// facilitate model checking machinery (property automata, stateful
			// variables to implement optimizations, etc...)
			for (Iterator<IPostNextStateBacktrackingInfo> metadataActions = tbi
					.getPostNextStateBacktrackingInfos().iterator(); metadataActions
					.hasNext();) {
				ISchedulingStrategyInfo ssi = metadataActions.next()
						.getSchedulingStrategyInfo();

				for (int i = 0; i < ssi.getInfoCount(); i++) {
					currNumOfChoices.add(ssi.getChoiceCount(i));
					currChosenIndices.add(ssi.getChosenIndex(i));
				}
			}

			// Now package up the scheduling info object for this transition

			result.add(new DefaultCounterExampleSchedulingInfo("State-"
					+ tbi.getStateId() + "-" + tbi.getInvisibleMoves(), tbi
					.getCanonicalThreadIndex(), currNumOfChoices.toArray(),
					currChosenIndices.toArray()));
		}

		return result;
	}

	protected void fillInitialVariableValues(IState vanillaState,
			IStateFactoryArguments args) {
		// Get bogus scheduling strategy context to use
		ISchedulingStrategyContext ssc = createContext(-1, -1, -1, vanillaState);
		ISchedulingStrategyInfo ssi = ss.newStrategyInfo();

		// Install the new context (none is yet installed)
		ee.setSchedulingStrategyContextInfo(ssc, ssi);

		// construct reverse (index --> name) globals identifier mapping
		IntObjectTable<String> globalNameMap = new IntObjectTable<String>();

		{
			for (String key : symbolTable.getGlobalIndexTable().keySet(true)) {
				globalNameMap.put(symbolTable.getGlobalIndexTable().get(key),
						key);
			}
		}

		ArrayList<Type> globalTypes = symbolTable.getGlobalTypes();
		int globalsCount = globalTypes.size();
		IValue[] globalValues = new IValue[globalsCount];

		for (int i = 0; i < globalsCount; i++) {
			String name = globalNameMap.get(i);
			Global astNode = (Global) symbolTable.getIdentifierDefTable().get(
					name);
			Type globalType = globalTypes.get(i);

			if (astNode.getOptionalValue() != null) {
				InitialValue initVal = astNode.getOptionalValue();

				IValue newValue = ee.evaluate(ssc, initVal.getValue(), ssi);

				if (astNode.getOptionalValue().getOptionalCoercedType() != null) {
					Type valueType = (Type) initVal.getValue().getProperty(
							Exp.TYPE);
					Type castType = (Type) initVal.getProperty(Exp.TYPE);

					newValue = ee.evaluateCast(castType, valueType, newValue);
				}

				vanillaState.setGlobalValue(i, newValue);
			}
		}

		for (int tid : vanillaState.getThreadIds()) {
			FSMSymbolTable fsmSymbolTable = symbolTable
					.getFSMSymbolTable(vanillaState.getLocation(tid));

			FSM fsm = fsmSymbolTable.getFSM();

			int argCount = fsm.getParamCount();
			int localCount = fsm.getLocalCount();

			for (int i = 0; i < localCount; i++) {
				Local astNode = fsm.getLocal(i);

				if (astNode.getOptionalValue() != null) {
					InitialValue initVal = astNode.getOptionalValue();

					IValue newValue = ee.evaluate(ssc, initVal.getValue(), ssi);

					if (astNode.getOptionalValue().getOptionalCoercedType() != null) {
						Type valueType = (Type) initVal.getValue().getProperty(
								Exp.TYPE);
						Type castType = (Type) initVal.getProperty(Exp.TYPE);

						newValue = ee.evaluateCast(castType, valueType,
								newValue);
					}

					vanillaState.setLocalValue(tid, argCount + i, newValue);
				}
			}
		}

		// uninstall bogus scheduling context
		ee.unsetSchedulingStrategyContextInfo();
	}

	protected ArrayList<Pair<Integer, Transformation>> makeChoices(
			IntObjectTable<ArrayList<Transformation>> ets) {
		int[] keys = ets.keys();
		int size = keys.length;
		Arrays.sort(keys);

		ArrayList<Pair<Integer, Transformation>> result = new ArrayList<Pair<Integer, Transformation>>();

		for (int i = 0; i < size; i++) {
			int threadId = keys[i];

			for (Transformation t : ets.get(threadId)) {
				result.add(new Pair<Integer, Transformation>(threadId, t));
			}
		}

		return result;
	}

	protected boolean shouldActivateThread(FSM fsm) {
		return fsm.getActive();
	}

	protected boolean shouldBacktrack() {
		ArrayList<ITransformationBacktrackingInfo> stack = sr
				.getBacktrackingInfos();

		if (stack.isEmpty()) {
			// If no transition executed yet, then obviously not...
			return false;
		} else {
			ITransformationBacktrackingInfo lastTbi = stack
					.get(stack.size() - 1);

			IEndStateBacktrackingInfo endStateMarker = Util.findLast(
					lastTbi.getNextStateBacktrackingInfos(),
					IEndStateBacktrackingInfo.class);
			IExceptionBacktrackingInfo exceptionMarker = Util.findLast(
					lastTbi.getNextStateBacktrackingInfos(),
					IExceptionBacktrackingInfo.class);

			if (endStateMarker != null) {
				return true;
			} else if (exceptionMarker != null) {
				BogorException mce = exceptionMarker.getThrownException();

				if (mce instanceof AssertionBogorException) {
					return true;
				} else if (mce instanceof RangeBogorException) {
					return true;
				} else if (mce instanceof ExtFailedBogorException) {
					return true;
				} else if (mce instanceof ExceptionThrownBogorException) {
					return exceptionMarker.isUncaught();
				}
			}
		}

		return false;
	}

	protected void storeCounterExample(
			ArrayList<ITransformationBacktrackingInfo> backtrackingInfos,
			int stateId, int invisibleMoves, String reason) {
		ArrayList<ICounterExampleSchedulingInfo> info = extractErrorSchedule(backtrackingInfos);
		cew.storeCounterExample(info, reason);
	}

	// ~ Classes
	// ................................................................

	protected class MaxErrorReachedException extends RuntimeException {
		// ~ Constructors
		// .......................................................

		public MaxErrorReachedException() {
		}
	}

	protected class FoundValueException extends RuntimeException {
		// ~ Constructors
		// .......................................................

		public FoundValueException() {
		}
	}

	/**
	 * @return a set of tuples whose first element says the name of the option,
	 *         and whose second element says whether the option is required, and
	 *         whose third element says whether the option is private to this
	 *         module (and thus prefixed by the interface implemented, e.g.,
	 *         <code>edu.ksu.cis.projects.bogor.module.ISearcher</code>) or
	 *         global in scope (and thus no qualifier is prepended).
	 */
	public Collection<Triple<String, Boolean, OptionScope>> getOptionIds() {
		ArrayList<Triple<String, Boolean, OptionScope>> result;
		result = new ArrayList<Triple<String, Boolean, OptionScope>>();

		for (String id : new String[] { PRINT_VERBOSE_TRACE_ID,
				WRITE_TRAIL_FILE_ID, PRINT_STATUS_ID,
				PRINT_COUNTER_EXAMPLES_ID, ALL_AS_ERRORS_ID, MAX_ERRORS_ID,
				MAX_DEPTH_ID, MAX_INVISIBLE_MOVES_ID,
				UPDATE_STATE_INCREMENT_ID, UPDATE_TRANSITION_INCREMENT_ID,
				INVARIANTS_ID, CHECK_BACKTRACK_ID }) {
			result.add(new Triple<String, Boolean, OptionScope>(id,
					Boolean.FALSE, OptionScope.MODULE));
		}

		return result;
	}

	/**
	 * @return a tuple whose first element says the domain of the option values,
	 *         and whose second element says whether the option is multivalued
	 *         (that is, a comma-separated list)
	 */
	public Pair<Domain, Boolean> getOptionDomain(String id) {
		if (PRINT_VERBOSE_TRACE_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (WRITE_TRAIL_FILE_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (PRINT_STATUS_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (PRINT_COUNTER_EXAMPLES_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (ALL_AS_ERRORS_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (CHECK_BACKTRACK_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
		} else if (MAX_ERRORS_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
		} else if (MAX_DEPTH_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
		} else if (MAX_INVISIBLE_MOVES_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
		} else if (UPDATE_STATE_INCREMENT_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
		} else if (UPDATE_TRANSITION_INCREMENT_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
		} else if (INVARIANTS_ID.equals(id)) {
			return new Pair<Domain, Boolean>(Domain.STRING, Boolean.TRUE);
		} else {
			return null;
		}
	}

	public Collection<String> getSuggestedValues(String id,
			IBogorConfiguration bc, SymbolTable st) {
		ArrayList<String> result = new ArrayList<String>();

		Pair<Domain, Boolean> domain = getOptionDomain(id);

		if (domain == null) {
			return result;
		}

		switch (domain.first) {
		case BOOLEAN:
			result.add(Boolean.toString(true));
			result.add(Boolean.toString(false));
			break;
		case INT:
			break;
		case STRING:
			if (INVARIANTS_ID.equals(id)) {
				Map<String, Type> funMap = st.getGlobalFunTable();

				for (String funId : funMap.keySet()) {
					Type type = funMap.get(funId);

					if (!(type instanceof FunType)) {
						continue;
					}

					FunType fType = (FunType) type;

					if (fType.getParamTypeCount() == 0
							&& fType.getReturnType() instanceof BooleanType) {
						result.add(funId);
					}
				}
			}
			break;
		default:
			break;
		}

		return result;
	}

	/**
	 * Checks whether the value of a configuration option is legal.
	 * 
	 * @param id
	 *            the option's name, as returned by the first tuple element of
	 *            an item returned by {@link #getOptionIds()}
	 * @param value
	 *            the value of the option, or <code>null</code> if unconfigued
	 * @param st
	 *            the symbol table for the BIR model
	 * @param errors
	 *            a container into which errors should be put. Implementors
	 *            should not assume that <code>errors</code> is empty upon entry
	 *            into this method; it may aggregate the results of calling
	 *            <code>validate</code> on many
	 *            <code>ISelfDescribingModule</code> instances.
	 * @return <code>true</code> iff the option is supported and its value is
	 *         legal
	 */
	public boolean validate(String id, String value, IBogorConfiguration bc,
			SymbolTable st, Collection<FileMessage> errors) {
		Pair<Domain, Boolean> domain = getOptionDomain(id);

		// If the option is unknown, then call it a bad value
		if (domain == null) {
			return false;
		}

		// No option in this module is required, so a blank value
		// will be considered OK
		if (value == null) {
			return true;
		}

		switch (domain.first) {
		case BOOLEAN:
			if (!"true".equalsIgnoreCase(value)
					&& !"false".equalsIgnoreCase(value)) {
				errors.add(FileMessage.buildMessage("Expecting boolean",
						new String[0]));
				return false;
			}
			break;
		case INT:
			try {
				int intValue = Integer.parseInt(value);

				if (intValue < 0) {
					errors.add(FileMessage.buildMessage("Must be non-negative",
							new String[0]));
					return false;
				}
			} catch (NumberFormatException nfe) {
				errors.add(FileMessage.buildMessage("Expecting int",
						new String[0]));
				return false;
			}
			break;
		case STRING:
			if (INVARIANTS_ID.equals(id)) {
				int beginErrorCount = errors.size();

				for (String funId : Util.splitCommaSeparatedList(value)) {
					Map<String, Type> funMap = st.getGlobalFunTable();

					Type type = funMap.get(funId);

					if (!(type instanceof FunType)) {
						errors.add(FileMessage.buildMessage("No such fun {0}",
								new String[] { funId }));
						continue;
					}

					FunType fType = (FunType) type;

					if (fType.getParamTypeCount() != 0
							|| !(fType.getReturnType() instanceof BooleanType)) {
						errors.add(FileMessage.buildMessage(
								"Expected {0} to be boolean, zero-arity",
								new String[] { funId }));
					}
				}

				if (errors.size() != beginErrorCount) {
					return false;
				}
			}
			break;
		default:
			break;
		}

		return true;
	}
}
